es:ES, P, Q:(E), T, T':Type, R:(TT').
(e:E. P(e)  (valtype(e) r T))
 (e:E. Q(e)  (valtype(e) r T'))
 ((e.P(e)  e.Q(e)) with R  ) 

latex

Definitions	(e.P(e)  e'.Q(e')) with R, x:A. B(x), x:A  B(x), (e.P(e) a.f(a) e'.Q(e')) with R, x. t(x), {x:A| B(x)} , P  Q, x(s), f(a), valtype(e), x:AB(x), E, x:A. B(x), , Type, t  T, ES
Lemmas	event system wf, es-E wf, es-valtype wf, causal-bijection wf